(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UF)
(declare-sort S0 0)
(declare-fun v0 () S0)
(declare-fun v1 () S0)
(declare-fun f0 ( S0) S0)
(declare-fun p0 ( S0) Bool)
(assert (let ((e2 (f0 v1)))
(let ((e3 (f0 v0)))
(let ((e4 (p0 e3)))
(let ((e5 (distinct v0 v1)))
(let ((e6 (p0 v0)))
(let ((e7 (p0 e3)))
(let ((e8 (p0 e3)))
(let ((e9 (p0 v1)))
(let ((e10 (= e2 v0)))
(let ((e11 (ite e5 v1 e3)))
(let ((e12 (ite e4 v0 v1)))
(let ((e13 (ite e7 e2 e3)))
(let ((e14 (ite e8 e12 e12)))
(let ((e15 (ite e10 e13 e12)))
(let ((e16 (ite e5 e11 e14)))
(let ((e17 (ite e9 e16 e12)))
(let ((e18 (ite e6 e15 e11)))
(let ((e19 (distinct v1 e15)))
(let ((e20 (p0 e13)))
(let ((e21 (p0 e12)))
(let ((e22 (distinct e17 e15)))
(let ((e23 (= v0 e16)))
(let ((e24 (distinct e2 e17)))
(let ((e25 (p0 e15)))
(let ((e26 (= e18 e14)))
(let ((e27 (p0 e12)))
(let ((e28 (p0 e13)))
(let ((e29 (distinct e11 e2)))
(let ((e30 (distinct e3 e16)))
(let ((e31 (ite e20 e9 e6)))
(let ((e32 (and e24 e19)))
(let ((e33 (xor e22 e22)))
(let ((e34 (ite e10 e5 e31)))
(let ((e35 (not e34)))
(let ((e36 (or e28 e33)))
(let ((e37 (= e4 e8)))
(let ((e38 (=> e23 e23)))
(let ((e39 (ite e37 e29 e30)))
(let ((e40 (not e39)))
(let ((e41 (xor e32 e40)))
(let ((e42 (= e21 e7)))
(let ((e43 (= e25 e25)))
(let ((e44 (= e35 e36)))
(let ((e45 (ite e43 e26 e38)))
(let ((e46 (and e42 e42)))
(let ((e47 (and e45 e41)))
(let ((e48 (or e27 e27)))
(let ((e49 (xor e48 e47)))
(let ((e50 (and e44 e46)))
(let ((e51 (not e49)))
(let ((e52 (=> e51 e50)))
e52
))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
